$\forall$$r$:CRng, $a$:Ideal($r$)\{i\}, $d$:detach\_fun($\mid$$r$$\mid$;$a$), $u$, $v$:$\mid$$r$$\mid$.
\\[0ex]($u$ = $v$ $\in$ Carrier($r$/$d$)) $\Leftarrow\!\Rightarrow$ ($\uparrow$($d$($u$ +$r$ ({-}$r$($v$)))))